\documentclass{article}


\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathpartir}

\usepackage{fullpage} % this is useful if you have wide derivations etc.

% Some commands
\newcommand{\eval}{\Downarrow}
\newcommand{\reduces}{\to}
\newcommand{\reducess}{\twoheadrightarrow}

\title{Example of evaluation and typing derivations in \LaTeX}

\begin{document}

\maketitle

\section{Inference rules}

\begin{mathpar}
\inferrule[E-Iszero]
{t \reduces t'}
{\texttt{iszero}\ t \reduces \texttt{iszero}\ t'}

\inferrule[E-IszeroZero]
{}
{\texttt{iszero 0} \reduces \texttt{true}}

\inferrule[E-IszeroSucc]
{}
{\texttt{iszero (succ}\ nv \texttt{)} \reduces \texttt{false}}

\inferrule[E-Succ]
{t \reduces t'}
{\texttt{succ}\ t \reduces \texttt{succ}\ t'}

\inferrule[E-Pred]
{t \reduces t'}
{\texttt{pred}\ t \reduces \texttt{pred}\ t'}

\inferrule[E-PredZero]
{}
{\texttt{pred}\ 0 \reduces \texttt{0}}

\inferrule[E-PredSucc]
{}
{\texttt{pred (succ}\ nv \texttt{)} \reduces nv}

\inferrule[E-IfTrue]
{}
{\texttt{if true then}\ t_2\ \texttt{else}\ t_3\ \reduces t_2}

\inferrule[E-IfFalse]
{}
{\texttt{if false then}\ t_2\ \texttt{else}\ t_3\ \reduces t_3}

\inferrule[E-If]
{t_1 \reduces t_1'}
{\texttt{if}\ t_1 \ \texttt{then}\ t_2\ \texttt{else}\ t_3\ \reduces 
 \texttt{if}\ t_1' \ \texttt{then}\ t_2\ \texttt{else}\ t_3}
\end{mathpar}


\section{Derivations}

\begin{mathpar}
\inferrule*[right=B-IfTrue]
{\inferrule*[right=B-True]{}{\texttt{true} \eval \texttt{true}} \\
 \inferrule*[right=B-False]{}{\texttt{false} \eval \texttt{false}} }
{\texttt{if true then false else true}\ \eval \texttt{false}}
\end{mathpar}

\begin{mathpar}
\inferrule*[right=B-IfFalse]
{\inferrule*[right=B-False]{}{\textsf{false} \eval \textsf{false}} \and
 \inferrule*[right=B-IfTrue]
  {
    \inferrule*[right=B-True]{}{\textsf{true} \eval \textsf{true}} \\
    \inferrule*[right=B-False]{}{\textsf{false} \eval \textsf{false}}}
  {\textsf{if true then false else true} \eval \textsf{false}} 
}
{\textsf{if false then true else (if true then false else true)}\ \eval \textsf{false}}
\end{mathpar}

\end{document}
